Nuprl Lemma : w-after-lemma 0,22

T:Type, w:World.
FairFifo  (e:E, x:Id. vartype(loc(e);x T  state_after(e).x = (x after e T
latex


Definitionst  T, #$n, x:AB(x), AB, n+m, a<b, Void, x:AB(x), P  Q, False, A, , {x:AB(x) }, , s(i;t).x, f(a), vartype(i;x), s = t, Prop, b, x:AB(x), E, time(e), loc(e), (x after e), s.x, state_after(e), Type, World, FairFifo, Id, <a,b>
Lemmasw-vartype wf, w-loc wf, Id wf, w-E wf, fair-fifo wf, world wf, w-state-after, w-s wf, le wf

origin